Nuprl Lemma : filter2_functionality
4,23
postcript
pdf
A
:Type,
L
:
A
List,
f1
,
f2
:(
||
L
||
).
f1
=
f2
filter2(
f2
;
L
) = filter2(
f1
;
L
)
A
List
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
filter2(
P
;
L
)
,
Prop
,
,
||
as
||
,
{
i
..
j
}
,
P
Q
Lemmas
int
seg
wf
,
length
wf1
,
bool
wf
,
filter2
wf
origin
A:Type, L:A List, f1, f2:(
||L||
). f1 = f2 
filter2(f2;L) = filter2(f1;L) 
A List A:Type, L:A List, f1, f2:(||L||). f1 = f2 filter2(f2;L) = filter2(f1;L) A List Tx:A. B(x)
} Q